E,X1,X2:Type, info:(E((:Id  X1) + (:(:IdLnk  E)  X2))), e:E.
(rcv?(e))  (sender(e)  E) 

latex

Definitions	x:A. B(x), P  Q, b, rcv?(e), t  T, sender(e), ecase1(e;info;i.f(i);l,e'.g(l;e')), ff, tt, t.2, t.1, if b then t else f fi , False, prop{i:l}
Lemmas	Id wf, IdLnk wf, false wf, true wf, assert wf, rcv? wf